Nuprl Definition : rel_plus
11,40
postcript
pdf
rel_plus(
T
;
R
)(
x
,
y
) ==
n
:
. (
x
rel_exp(
T
;
R
;
n
)
y
)
latex
Definitions
x
.
A
(
x
)
,
x
:
A
.
B
(
x
)
,
,
x
f
y
,
rel_exp(
T
;
R
;
n
)
FDL editor aliases
rel_plus
origin
n:
. (x rel_exp(T; R; n) y) n:. (x rel_exp(T; R; n) y) 
x.A(x)x:A. B(x)